(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status unknown)
(set-logic QF_LRA)
(declare-fun v0 () Real)
(declare-fun v1 () Real)
(declare-fun v2 () Real)
(assert (let ((e3 1))
(let ((e4 6))
(let ((e5 (/ e3 e3)))
(let ((e6 (- e5)))
(let ((e7 (/ e3 (- e4))))
(let ((e8 (- v2)))
(let ((e9 (+ v2 e6)))
(let ((e10 (- e8 v0)))
(let ((e11 (/ e3 (- e3))))
(let ((e12 (+ v0 e7)))
(let ((e13 (- v1 v1)))
(let ((e14 (< e12 v0)))
(let ((e15 (= e11 v0)))
(let ((e16 (= v1 e10)))
(let ((e17 (< e10 e5)))
(let ((e18 (> e10 e7)))
(let ((e19 (<= v1 v2)))
(let ((e20 (= e7 e12)))
(let ((e21 (< e6 e13)))
(let ((e22 (= e7 e8)))
(let ((e23 (< e6 e11)))
(let ((e24 (< e11 e9)))
(let ((e25 (ite e14 e6 e7)))
(let ((e26 (ite e17 v1 v1)))
(let ((e27 (ite e24 e11 e13)))
(let ((e28 (ite e18 e9 e5)))
(let ((e29 (ite e18 v0 e9)))
(let ((e30 (ite e21 e10 e5)))
(let ((e31 (ite e14 e12 v2)))
(let ((e32 (ite e22 e5 e7)))
(let ((e33 (ite e20 v0 v2)))
(let ((e34 (ite e16 e8 e9)))
(let ((e35 (ite e23 e28 e8)))
(let ((e36 (ite e19 e33 e9)))
(let ((e37 (ite e24 e36 e35)))
(let ((e38 (ite e15 e13 e25)))
(let ((e39 (distinct e9 e38)))
(let ((e40 (<= e27 e5)))
(let ((e41 (= e13 v2)))
(let ((e42 (= v1 e36)))
(let ((e43 (>= e6 e8)))
(let ((e44 (>= e37 e9)))
(let ((e45 (>= e38 e33)))
(let ((e46 (< v2 e5)))
(let ((e47 (< e37 v0)))
(let ((e48 (distinct e13 v2)))
(let ((e49 (>= e36 e34)))
(let ((e50 (<= v2 e30)))
(let ((e51 (< e37 e8)))
(let ((e52 (<= e12 e13)))
(let ((e53 (>= v0 e12)))
(let ((e54 (<= v0 e38)))
(let ((e55 (distinct e36 e10)))
(let ((e56 (< e8 e29)))
(let ((e57 (= e29 e12)))
(let ((e58 (>= e33 e26)))
(let ((e59 (>= e32 e28)))
(let ((e60 (distinct e38 e31)))
(let ((e61 (>= e36 e36)))
(let ((e62 (> v1 e11)))
(let ((e63 (= e7 e10)))
(let ((e64 (< v2 e11)))
(let ((e65 (= e7 e35)))
(let ((e66 (< e30 e35)))
(let ((e67 (<= e32 e25)))
(let ((e68 (= e23 e60)))
(let ((e69 (not e43)))
(let ((e70 (and e56 e55)))
(let ((e71 (ite e54 e18 e48)))
(let ((e72 (ite e47 e63 e49)))
(let ((e73 (not e20)))
(let ((e74 (or e62 e62)))
(let ((e75 (= e39 e64)))
(let ((e76 (= e59 e70)))
(let ((e77 (not e44)))
(let ((e78 (and e77 e68)))
(let ((e79 (ite e22 e57 e52)))
(let ((e80 (not e15)))
(let ((e81 (ite e79 e45 e74)))
(let ((e82 (xor e16 e75)))
(let ((e83 (ite e66 e78 e66)))
(let ((e84 (= e61 e42)))
(let ((e85 (=> e67 e72)))
(let ((e86 (= e17 e19)))
(let ((e87 (or e84 e76)))
(let ((e88 (= e41 e51)))
(let ((e89 (= e85 e81)))
(let ((e90 (ite e71 e83 e71)))
(let ((e91 (or e53 e46)))
(let ((e92 (=> e88 e89)))
(let ((e93 (xor e24 e86)))
(let ((e94 (ite e91 e92 e14)))
(let ((e95 (ite e40 e40 e50)))
(let ((e96 (not e21)))
(let ((e97 (not e69)))
(let ((e98 (xor e87 e97)))
(let ((e99 (=> e94 e93)))
(let ((e100 (xor e82 e99)))
(let ((e101 (xor e96 e65)))
(let ((e102 (and e95 e100)))
(let ((e103 (not e98)))
(let ((e104 (and e80 e90)))
(let ((e105 (ite e73 e103 e58)))
(let ((e106 (xor e102 e105)))
(let ((e107 (xor e104 e104)))
(let ((e108 (and e106 e101)))
(let ((e109 (or e108 e107)))
e109
))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

(check-sat)
